$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $x$,$y$:$A$, $v$:top. ($\uparrow$fpf{-}dom(${\it eq}$; $x$; fpf{-}single($y$; $v$))) $\Leftarrow\!\Rightarrow$ ($x$ = $y$)